Termination proof of /tmp/tmpTW11uN/SharingAnalysis.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 1510 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 420 ms)

        ↳7 IDP

        ↳8 IDPtoQDPProof (⇒, 0 ms)

        ↳9 QDP

        ↳10 QDPSizeChangeProof (⇔, 0 ms)

        ↳11 YES

    ↳12 JBCTerminationSCC

        ↳13 SCCToIDPv1Proof (⇒, 90 ms)

        ↳14 IDP

        ↳15 IDPNonInfProof (⇒, 140 ms)

        ↳16 AND

            ↳17 IDP

                ↳18 IDependencyGraphProof (⇔, 0 ms)

                ↳19 TRUE

            ↳20 IDP

                ↳21 IDependencyGraphProof (⇔, 0 ms)

                ↳22 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_25 (Sun Microsystems Inc.) Main-Class: SharingAnalysis/SharingAnalysis

package SharingAnalysis;

public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
    final String string = args[index];
    index++;
    return string.length();
  }
}


package SharingAnalysis;

public class SharingAnalysis {
	int val;
	SharingAnalysis field;

	public static void main(String[] args) {
		Random.args = args;
		SharingAnalysis t1 = new SharingAnalysis();
		SharingAnalysis t2 = t1.appendNewList(1);
		SharingAnalysis t3 = t2.appendNewList(Random.random());
		t2.field = null;
		copy(t1, t3);
	}

	public static void copy(SharingAnalysis source, SharingAnalysis target) {
		while (source != null) {
			SharingAnalysis newEle = new SharingAnalysis();
			newEle.val = source.val;
			target.field = newEle;
			source = source.field;
			target = target.field;
		}
	}

	/**
 	 * @param i number of elements to append
 	 * @return the last list element appended
 	 */
	private SharingAnalysis appendNewList(int i) {
		this.field = new SharingAnalysis();
		SharingAnalysis cur = this.field;
		while (i > 1) {
			i--;
			cur = cur.field = new SharingAnalysis();
		}
		return cur;
	}
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
SharingAnalysis.SharingAnalysis.main([Ljava/lang/String;)V: Graph of 259 nodes with 2 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: SharingAnalysis.SharingAnalysis.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 88 rules for P and 0 rules for R.

P rules:
1283_0_copy_NULL(EOS(STATIC_1283), java.lang.Object(o1219sub), java.lang.Object(o1229sub), java.lang.Object(o1229sub)) → 1285_0_copy_NULL(EOS(STATIC_1285), java.lang.Object(o1219sub), java.lang.Object(o1229sub), java.lang.Object(o1229sub))
1285_0_copy_NULL(EOS(STATIC_1285), java.lang.Object(o1219sub), java.lang.Object(o1229sub), java.lang.Object(o1229sub)) → 1288_0_copy_New(EOS(STATIC_1288), java.lang.Object(o1219sub), java.lang.Object(o1229sub))
1288_0_copy_New(EOS(STATIC_1288), java.lang.Object(o1219sub), java.lang.Object(o1229sub)) → 1291_0_copy_Duplicate(EOS(STATIC_1291), java.lang.Object(o1219sub), java.lang.Object(o1229sub))
1291_0_copy_Duplicate(EOS(STATIC_1291), java.lang.Object(o1219sub), java.lang.Object(o1229sub)) → 1294_0_copy_InvokeMethod(EOS(STATIC_1294), java.lang.Object(o1219sub), java.lang.Object(o1229sub))
1294_0_copy_InvokeMethod(EOS(STATIC_1294), java.lang.Object(o1219sub), java.lang.Object(o1229sub)) → 1297_0_<init>_Load(EOS(STATIC_1297), java.lang.Object(o1219sub), java.lang.Object(o1229sub))
1297_0_<init>_Load(EOS(STATIC_1297), java.lang.Object(o1219sub), java.lang.Object(o1229sub)) → 1300_0_<init>_InvokeMethod(EOS(STATIC_1300), java.lang.Object(o1219sub), java.lang.Object(o1229sub))
1300_0_<init>_InvokeMethod(EOS(STATIC_1300), java.lang.Object(o1219sub), java.lang.Object(o1229sub)) → 1303_0_<init>_Return(EOS(STATIC_1303), java.lang.Object(o1219sub), java.lang.Object(o1229sub))
1303_0_<init>_Return(EOS(STATIC_1303), java.lang.Object(o1219sub), java.lang.Object(o1229sub)) → 1305_0_copy_Store(EOS(STATIC_1305), java.lang.Object(o1219sub), java.lang.Object(o1229sub))
1305_0_copy_Store(EOS(STATIC_1305), java.lang.Object(o1219sub), java.lang.Object(o1229sub)) → 1306_0_copy_Load(EOS(STATIC_1306), java.lang.Object(o1219sub), java.lang.Object(o1229sub))
1306_0_copy_Load(EOS(STATIC_1306), java.lang.Object(o1219sub), java.lang.Object(o1229sub)) → 1308_0_copy_Load(EOS(STATIC_1308), java.lang.Object(o1219sub), java.lang.Object(o1229sub))
1308_0_copy_Load(EOS(STATIC_1308), java.lang.Object(o1219sub), java.lang.Object(o1229sub)) → 1311_0_copy_FieldAccess(EOS(STATIC_1311), java.lang.Object(o1219sub), java.lang.Object(o1229sub), java.lang.Object(o1229sub))
1311_0_copy_FieldAccess(EOS(STATIC_1311), java.lang.Object(o1219sub), java.lang.Object(o1229sub), java.lang.Object(o1229sub)) → 1314_0_copy_FieldAccess(EOS(STATIC_1314), java.lang.Object(o1219sub), java.lang.Object(o1229sub), java.lang.Object(o1229sub))
1311_0_copy_FieldAccess(EOS(STATIC_1311), java.lang.Object(o1219sub), java.lang.Object(o1219sub), java.lang.Object(o1219sub)) → 1315_0_copy_FieldAccess(EOS(STATIC_1315), java.lang.Object(o1219sub), java.lang.Object(o1219sub), java.lang.Object(o1219sub))
1314_0_copy_FieldAccess(EOS(STATIC_1314), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1317_0_copy_FieldAccess(EOS(STATIC_1317), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)))
1317_0_copy_FieldAccess(EOS(STATIC_1317), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1320_0_copy_FieldAccess(EOS(STATIC_1320), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)))
1320_0_copy_FieldAccess(EOS(STATIC_1320), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1325_0_copy_Load(EOS(STATIC_1325), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)))
1325_0_copy_Load(EOS(STATIC_1325), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1329_0_copy_Load(EOS(STATIC_1329), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)))
1329_0_copy_Load(EOS(STATIC_1329), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1334_0_copy_FieldAccess(EOS(STATIC_1334), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)))
1334_0_copy_FieldAccess(EOS(STATIC_1334), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1341_0_copy_FieldAccess(EOS(STATIC_1341), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)))
1334_0_copy_FieldAccess(EOS(STATIC_1334), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1342_0_copy_FieldAccess(EOS(STATIC_1342), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)))
1341_0_copy_FieldAccess(EOS(STATIC_1341), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1348_0_copy_FieldAccess(EOS(STATIC_1348), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)))
1348_0_copy_FieldAccess(EOS(STATIC_1348), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1359_0_copy_FieldAccess(EOS(STATIC_1359), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)))
1348_0_copy_FieldAccess(EOS(STATIC_1348), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1360_0_copy_FieldAccess(EOS(STATIC_1360), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)))
1359_0_copy_FieldAccess(EOS(STATIC_1359), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1371_0_copy_Load(EOS(STATIC_1371), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)))
1371_0_copy_Load(EOS(STATIC_1371), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1396_0_copy_FieldAccess(EOS(STATIC_1396), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)))
1396_0_copy_FieldAccess(EOS(STATIC_1396), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1421_0_copy_Store(EOS(STATIC_1421), java.lang.Object(o1219sub), o1240)
1421_0_copy_Store(EOS(STATIC_1421), java.lang.Object(o1219sub), o1240) → 1444_0_copy_Load(EOS(STATIC_1444), java.lang.Object(o1219sub), o1240)
1444_0_copy_Load(EOS(STATIC_1444), java.lang.Object(o1219sub), o1240) → 1466_0_copy_FieldAccess(EOS(STATIC_1466), java.lang.Object(o1219sub), o1240)
1466_0_copy_FieldAccess(EOS(STATIC_1466), java.lang.Object(o1219sub), o1240) → 1482_0_copy_Store(EOS(STATIC_1482), java.lang.Object(o1219sub), o1240)
1482_0_copy_Store(EOS(STATIC_1482), java.lang.Object(o1219sub), o1240) → 1507_0_copy_JMP(EOS(STATIC_1507), java.lang.Object(o1219sub), o1240)
1507_0_copy_JMP(EOS(STATIC_1507), java.lang.Object(o1219sub), o1240) → 1971_0_copy_Load(EOS(STATIC_1971), java.lang.Object(o1219sub), o1240)
1971_0_copy_Load(EOS(STATIC_1971), java.lang.Object(o1219sub), o1240) → 1279_0_copy_Load(EOS(STATIC_1279), java.lang.Object(o1219sub), o1240)
1279_0_copy_Load(EOS(STATIC_1279), java.lang.Object(o1219sub), o1216) → 1283_0_copy_NULL(EOS(STATIC_1283), java.lang.Object(o1219sub), o1216, o1216)
1360_0_copy_FieldAccess(EOS(STATIC_1360), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1372_0_copy_Load(EOS(STATIC_1372), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)))
1372_0_copy_Load(EOS(STATIC_1372), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1400_0_copy_FieldAccess(EOS(STATIC_1400), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)))
1400_0_copy_FieldAccess(EOS(STATIC_1400), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1426_0_copy_Store(EOS(STATIC_1426), java.lang.Object(o1219sub), o1240)
1426_0_copy_Store(EOS(STATIC_1426), java.lang.Object(o1219sub), o1240) → 1448_0_copy_Load(EOS(STATIC_1448), java.lang.Object(o1219sub), o1240)
1448_0_copy_Load(EOS(STATIC_1448), java.lang.Object(o1219sub), o1240) → 1471_0_copy_FieldAccess(EOS(STATIC_1471), java.lang.Object(o1219sub), o1240)
1471_0_copy_FieldAccess(EOS(STATIC_1471), java.lang.Object(o1219sub), o1240) → 1486_0_copy_Store(EOS(STATIC_1486), java.lang.Object(o1219sub), o1240)
1486_0_copy_Store(EOS(STATIC_1486), java.lang.Object(o1219sub), o1240) → 1511_0_copy_JMP(EOS(STATIC_1511), java.lang.Object(o1219sub), o1240)
1511_0_copy_JMP(EOS(STATIC_1511), java.lang.Object(o1219sub), o1240) → 1975_0_copy_Load(EOS(STATIC_1975), java.lang.Object(o1219sub), o1240)
1975_0_copy_Load(EOS(STATIC_1975), java.lang.Object(o1219sub), o1240) → 1279_0_copy_Load(EOS(STATIC_1279), java.lang.Object(o1219sub), o1240)
1342_0_copy_FieldAccess(EOS(STATIC_1342), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1351_0_copy_Load(EOS(STATIC_1351), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)))
1351_0_copy_Load(EOS(STATIC_1351), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1362_0_copy_FieldAccess(EOS(STATIC_1362), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240)))
1362_0_copy_FieldAccess(EOS(STATIC_1362), java.lang.Object(o1219sub), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i165, o1240))) → 1374_0_copy_Store(EOS(STATIC_1374), java.lang.Object(o1219sub), o1240)
1374_0_copy_Store(EOS(STATIC_1374), java.lang.Object(o1219sub), o1240) → 1402_0_copy_Load(EOS(STATIC_1402), java.lang.Object(o1219sub), o1240)
1402_0_copy_Load(EOS(STATIC_1402), java.lang.Object(o1219sub), o1240) → 1427_0_copy_FieldAccess(EOS(STATIC_1427), java.lang.Object(o1219sub), o1240)
1427_0_copy_FieldAccess(EOS(STATIC_1427), java.lang.Object(o1219sub), o1240) → 1450_0_copy_Store(EOS(STATIC_1450), java.lang.Object(o1219sub), o1240)
1450_0_copy_Store(EOS(STATIC_1450), java.lang.Object(o1219sub), o1240) → 1472_0_copy_JMP(EOS(STATIC_1472), java.lang.Object(o1219sub), o1240)
1472_0_copy_JMP(EOS(STATIC_1472), java.lang.Object(o1219sub), o1240) → 1490_0_copy_Load(EOS(STATIC_1490), java.lang.Object(o1219sub), o1240)
1490_0_copy_Load(EOS(STATIC_1490), java.lang.Object(o1219sub), o1240) → 1279_0_copy_Load(EOS(STATIC_1279), java.lang.Object(o1219sub), o1240)
1315_0_copy_FieldAccess(EOS(STATIC_1315), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1319_0_copy_FieldAccess(EOS(STATIC_1319), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)))
1319_0_copy_FieldAccess(EOS(STATIC_1319), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1323_0_copy_FieldAccess(EOS(STATIC_1323), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)))
1323_0_copy_FieldAccess(EOS(STATIC_1323), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1328_0_copy_Load(EOS(STATIC_1328), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)))
1328_0_copy_Load(EOS(STATIC_1328), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1331_0_copy_Load(EOS(STATIC_1331), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)))
1331_0_copy_Load(EOS(STATIC_1331), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1339_0_copy_FieldAccess(EOS(STATIC_1339), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)))
1339_0_copy_FieldAccess(EOS(STATIC_1339), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1345_0_copy_FieldAccess(EOS(STATIC_1345), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)))
1339_0_copy_FieldAccess(EOS(STATIC_1339), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1346_0_copy_FieldAccess(EOS(STATIC_1346), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)))
1345_0_copy_FieldAccess(EOS(STATIC_1345), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1353_0_copy_FieldAccess(EOS(STATIC_1353), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)))
1353_0_copy_FieldAccess(EOS(STATIC_1353), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1365_0_copy_FieldAccess(EOS(STATIC_1365), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)))
1353_0_copy_FieldAccess(EOS(STATIC_1353), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1366_0_copy_FieldAccess(EOS(STATIC_1366), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)))
1365_0_copy_FieldAccess(EOS(STATIC_1365), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1381_0_copy_Load(EOS(STATIC_1381), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)))
1381_0_copy_Load(EOS(STATIC_1381), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1408_0_copy_FieldAccess(EOS(STATIC_1408), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)))
1408_0_copy_FieldAccess(EOS(STATIC_1408), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1433_0_copy_Store(EOS(STATIC_1433), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1433_0_copy_Store(EOS(STATIC_1433), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1455_0_copy_Load(EOS(STATIC_1455), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1455_0_copy_Load(EOS(STATIC_1455), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1475_0_copy_FieldAccess(EOS(STATIC_1475), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1475_0_copy_FieldAccess(EOS(STATIC_1475), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1495_0_copy_Store(EOS(STATIC_1495), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1495_0_copy_Store(EOS(STATIC_1495), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1697_0_copy_JMP(EOS(STATIC_1697), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1697_0_copy_JMP(EOS(STATIC_1697), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1979_0_copy_Load(EOS(STATIC_1979), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1979_0_copy_Load(EOS(STATIC_1979), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1279_0_copy_Load(EOS(STATIC_1279), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1366_0_copy_FieldAccess(EOS(STATIC_1366), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1390_0_copy_Load(EOS(STATIC_1390), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)))
1390_0_copy_Load(EOS(STATIC_1390), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1415_0_copy_FieldAccess(EOS(STATIC_1415), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)))
1415_0_copy_FieldAccess(EOS(STATIC_1415), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1440_0_copy_Store(EOS(STATIC_1440), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1440_0_copy_Store(EOS(STATIC_1440), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1461_0_copy_Load(EOS(STATIC_1461), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1461_0_copy_Load(EOS(STATIC_1461), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1476_0_copy_FieldAccess(EOS(STATIC_1476), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1476_0_copy_FieldAccess(EOS(STATIC_1476), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1501_0_copy_Store(EOS(STATIC_1501), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1501_0_copy_Store(EOS(STATIC_1501), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1701_0_copy_JMP(EOS(STATIC_1701), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1701_0_copy_JMP(EOS(STATIC_1701), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1983_0_copy_Load(EOS(STATIC_1983), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1983_0_copy_Load(EOS(STATIC_1983), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1279_0_copy_Load(EOS(STATIC_1279), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1346_0_copy_FieldAccess(EOS(STATIC_1346), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1357_0_copy_Load(EOS(STATIC_1357), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)))
1357_0_copy_Load(EOS(STATIC_1357), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1369_0_copy_FieldAccess(EOS(STATIC_1369), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)))
1369_0_copy_FieldAccess(EOS(STATIC_1369), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242))) → 1393_0_copy_Store(EOS(STATIC_1393), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1393_0_copy_Store(EOS(STATIC_1393), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1417_0_copy_Load(EOS(STATIC_1417), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1417_0_copy_Load(EOS(STATIC_1417), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1441_0_copy_FieldAccess(EOS(STATIC_1441), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1441_0_copy_FieldAccess(EOS(STATIC_1441), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1464_0_copy_Store(EOS(STATIC_1464), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1464_0_copy_Store(EOS(STATIC_1464), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1478_0_copy_JMP(EOS(STATIC_1478), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1478_0_copy_JMP(EOS(STATIC_1478), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1504_0_copy_Load(EOS(STATIC_1504), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
1504_0_copy_Load(EOS(STATIC_1504), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242) → 1279_0_copy_Load(EOS(STATIC_1279), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, i166, o1242)), o1242)
R rules:

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
1283_0_copy_NULL(EOS(STATIC_1283), java.lang.Object(x0), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x1, x2)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x1, x2))) → 1283_0_copy_NULL(EOS(STATIC_1283), java.lang.Object(x0), x2, x2)
1283_0_copy_NULL(EOS(STATIC_1283), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x0, x1)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x0, x1)), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x0, x1))) → 1283_0_copy_NULL(EOS(STATIC_1283), java.lang.Object(SharingAnalysis.SharingAnalysis(EOC, x0, x1)), x1, x1)
R rules:

Filtered ground terms:

1283_0_copy_NULL(x1, x2, x3, x4) → 1283_0_copy_NULL(x2, x3, x4)
SharingAnalysis.SharingAnalysis(x1, x2, x3) → SharingAnalysis.SharingAnalysis(x2, x3)
EOS(x1) → EOS

Filtered duplicate args:

1283_0_copy_NULL(x1, x2, x3) → 1283_0_copy_NULL(x1, x3)

Filtered unneeded arguments:

SharingAnalysis.SharingAnalysis(x1, x2) → SharingAnalysis.SharingAnalysis(x2)

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
1283_0_copy_NULL(java.lang.Object(x0), java.lang.Object(SharingAnalysis.SharingAnalysis(x2))) → 1283_0_copy_NULL(java.lang.Object(x0), x2)
1283_0_copy_NULL(java.lang.Object(SharingAnalysis.SharingAnalysis(x1)), java.lang.Object(SharingAnalysis.SharingAnalysis(x1))) → 1283_0_copy_NULL(java.lang.Object(SharingAnalysis.SharingAnalysis(x1)), x1)
R rules:

Finished conversion. Obtained 2 rules for P and 0 rules for R. System has no predefined symbols.

P rules:
1283_0_COPY_NULL(java.lang.Object(x0), java.lang.Object(SharingAnalysis.SharingAnalysis(x2))) → 1283_0_COPY_NULL(java.lang.Object(x0), x2)
1283_0_COPY_NULL(java.lang.Object(SharingAnalysis.SharingAnalysis(x1)), java.lang.Object(SharingAnalysis.SharingAnalysis(x1))) → 1283_0_COPY_NULL(java.lang.Object(SharingAnalysis.SharingAnalysis(x1)), x1)
R rules:

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none

R is empty.

The integer pair graph contains the following rules and edges:
(0): 1283_0_COPY_NULL(java.lang.Object(x0[0]), java.lang.Object(SharingAnalysis.SharingAnalysis(x2[0]))) → 1283_0_COPY_NULL(java.lang.Object(x0[0]), x2[0])
(1): 1283_0_COPY_NULL(java.lang.Object(SharingAnalysis.SharingAnalysis(x1[1])), java.lang.Object(SharingAnalysis.SharingAnalysis(x1[1]))) → 1283_0_COPY_NULL(java.lang.Object(SharingAnalysis.SharingAnalysis(x1[1])), x1[1])

(0) -> (0), if (java.lang.Object(x0[0]) →^* java.lang.Object(x0[0]')∧x2[0] →^* java.lang.Object(SharingAnalysis.SharingAnalysis(x2[0]')))

(0) -> (1), if (java.lang.Object(x0[0]) →^* java.lang.Object(SharingAnalysis.SharingAnalysis(x1[1]))∧x2[0] →^* java.lang.Object(SharingAnalysis.SharingAnalysis(x1[1])))

(1) -> (0), if (java.lang.Object(SharingAnalysis.SharingAnalysis(x1[1])) →^* java.lang.Object(x0[0])∧x1[1] →^* java.lang.Object(SharingAnalysis.SharingAnalysis(x2[0])))

(1) -> (1), if (java.lang.Object(SharingAnalysis.SharingAnalysis(x1[1])) →^* java.lang.Object(SharingAnalysis.SharingAnalysis(x1[1]'))∧x1[1] →^* java.lang.Object(SharingAnalysis.SharingAnalysis(x1[1]')))

The set Q is empty.

(8) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

1283_0_COPY_NULL(java.lang.Object(x0[0]), java.lang.Object(SharingAnalysis.SharingAnalysis(x2[0]))) → 1283_0_COPY_NULL(java.lang.Object(x0[0]), x2[0])
1283_0_COPY_NULL(java.lang.Object(SharingAnalysis.SharingAnalysis(x1[1])), java.lang.Object(SharingAnalysis.SharingAnalysis(x1[1]))) → 1283_0_COPY_NULL(java.lang.Object(SharingAnalysis.SharingAnalysis(x1[1])), x1[1])

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(10) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

1283_0_COPY_NULL(java.lang.Object(x0[0]), java.lang.Object(SharingAnalysis.SharingAnalysis(x2[0]))) → 1283_0_COPY_NULL(java.lang.Object(x0[0]), x2[0])
The graph contains the following edges 1 >= 1, 2 > 2
1283_0_COPY_NULL(java.lang.Object(SharingAnalysis.SharingAnalysis(x1[1])), java.lang.Object(SharingAnalysis.SharingAnalysis(x1[1]))) → 1283_0_COPY_NULL(java.lang.Object(SharingAnalysis.SharingAnalysis(x1[1])), x1[1])
The graph contains the following edges 1 >= 1, 2 >= 1, 1 > 2, 2 > 2

(11) YES

(12) Obligation:

(13) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 23 rules for P and 0 rules for R.

P rules:
398_0_appendNewList_ConstantStackPush(EOS(STATIC_398), i32, i32) → 402_0_appendNewList_LE(EOS(STATIC_402), i32, i32, 1)
402_0_appendNewList_LE(EOS(STATIC_402), i47, i47, matching1) → 406_0_appendNewList_LE(EOS(STATIC_406), i47, i47, 1) | =(matching1, 1)
406_0_appendNewList_LE(EOS(STATIC_406), i47, i47, matching1) → 410_0_appendNewList_Inc(EOS(STATIC_410), i47) | &&(>(i47, 1), =(matching1, 1))
410_0_appendNewList_Inc(EOS(STATIC_410), i47) → 414_0_appendNewList_Load(EOS(STATIC_414), +(i47, -1)) | >(i47, 0)
414_0_appendNewList_Load(EOS(STATIC_414), i48) → 419_0_appendNewList_New(EOS(STATIC_419), i48)
419_0_appendNewList_New(EOS(STATIC_419), i48) → 423_0_appendNewList_Duplicate(EOS(STATIC_423), i48)
423_0_appendNewList_Duplicate(EOS(STATIC_423), i48) → 428_0_appendNewList_InvokeMethod(EOS(STATIC_428), i48)
428_0_appendNewList_InvokeMethod(EOS(STATIC_428), i48) → 431_0_<init>_Load(EOS(STATIC_431), i48)
431_0_<init>_Load(EOS(STATIC_431), i48) → 439_0_<init>_InvokeMethod(EOS(STATIC_439), i48)
439_0_<init>_InvokeMethod(EOS(STATIC_439), i48) → 444_0_<init>_Return(EOS(STATIC_444), i48)
444_0_<init>_Return(EOS(STATIC_444), i48) → 448_0_appendNewList_Duplicate(EOS(STATIC_448), i48)
448_0_appendNewList_Duplicate(EOS(STATIC_448), i48) → 453_0_appendNewList_FieldAccess(EOS(STATIC_453), i48)
453_0_appendNewList_FieldAccess(EOS(STATIC_453), i48) → 459_0_appendNewList_FieldAccess(EOS(STATIC_459), i48)
453_0_appendNewList_FieldAccess(EOS(STATIC_453), i48) → 460_0_appendNewList_FieldAccess(EOS(STATIC_460), i48)
459_0_appendNewList_FieldAccess(EOS(STATIC_459), i48) → 464_0_appendNewList_Store(EOS(STATIC_464), i48)
464_0_appendNewList_Store(EOS(STATIC_464), i48) → 474_0_appendNewList_JMP(EOS(STATIC_474), i48)
474_0_appendNewList_JMP(EOS(STATIC_474), i48) → 496_0_appendNewList_Load(EOS(STATIC_496), i48)
496_0_appendNewList_Load(EOS(STATIC_496), i48) → 393_0_appendNewList_Load(EOS(STATIC_393), i48)
393_0_appendNewList_Load(EOS(STATIC_393), i32) → 398_0_appendNewList_ConstantStackPush(EOS(STATIC_398), i32, i32)
460_0_appendNewList_FieldAccess(EOS(STATIC_460), i48) → 469_0_appendNewList_Store(EOS(STATIC_469), i48)
469_0_appendNewList_Store(EOS(STATIC_469), i48) → 478_0_appendNewList_JMP(EOS(STATIC_478), i48)
478_0_appendNewList_JMP(EOS(STATIC_478), i48) → 506_0_appendNewList_Load(EOS(STATIC_506), i48)
506_0_appendNewList_Load(EOS(STATIC_506), i48) → 393_0_appendNewList_Load(EOS(STATIC_393), i48)
R rules:

Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.

P rules:
398_0_appendNewList_ConstantStackPush(EOS(STATIC_398), x0, x0) → 398_0_appendNewList_ConstantStackPush(EOS(STATIC_398), +(x0, -1), +(x0, -1)) | >(x0, 1)
R rules:

Filtered ground terms:

398_0_appendNewList_ConstantStackPush(x1, x2, x3) → 398_0_appendNewList_ConstantStackPush(x2, x3)
EOS(x1) → EOS
Cond_398_0_appendNewList_ConstantStackPush(x1, x2, x3, x4) → Cond_398_0_appendNewList_ConstantStackPush(x1, x3, x4)

Filtered duplicate args:

398_0_appendNewList_ConstantStackPush(x1, x2) → 398_0_appendNewList_ConstantStackPush(x2)
Cond_398_0_appendNewList_ConstantStackPush(x1, x2, x3) → Cond_398_0_appendNewList_ConstantStackPush(x1, x3)

Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.

P rules:
398_0_appendNewList_ConstantStackPush(x0) → 398_0_appendNewList_ConstantStackPush(+(x0, -1)) | >(x0, 1)
R rules:

Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.

P rules:
398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(x0) → COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(>(x0, 1), x0)
COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(TRUE, x0) → 398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(+(x0, -1))
R rules:

(14) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(x0[0]) → COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(x0[0] > 1, x0[0])
(1): COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(TRUE, x0[1]) → 398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(x0[1] + -1)

(0) -> (1), if (x0[0] > 1 ∧x0[0] →^* x0[1])

(1) -> (0), if (x0[1] + -1 →^* x0[0])

The set Q is empty.

(15) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@649ebbfd Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(x0) → COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(>(x0, 1), x0) the following chains were created:

We consider the chain 398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(x0[0]) → COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(>(x0[0], 1), x0[0]), COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(TRUE, x0[1]) → 398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(+(x0[1], -1)) which results in the following constraint:
(1)    (>(x0[0], 1)=TRUE∧x0[0]=x0[1] ⇒ 398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(x0[0])≥NonInfC∧398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(x0[0])≥COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(>(x0[0], 1), x0[0])∧(U^Increasing(COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(>(x0[0], 1), x0[0])), ≥))

We simplified constraint (1) using rule (IV) which results in the following new constraint:
(2)    (>(x0[0], 1)=TRUE ⇒ 398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(x0[0])≥NonInfC∧398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(x0[0])≥COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(>(x0[0], 1), x0[0])∧(U^Increasing(COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(>(x0[0], 1), x0[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(>(x0[0], 1), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(>(x0[0], 1), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-2] ≥ 0 ⇒ (U^Increasing(COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(>(x0[0], 1), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0 ⇒ (U^Increasing(COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(>(x0[0], 1), x0[0])), ≥)∧[(-1)Bound*bni_8 + (4)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

For Pair COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(TRUE, x0) → 398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(+(x0, -1)) the following chains were created:

We consider the chain COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(TRUE, x0[1]) → 398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(+(x0[1], -1)) which results in the following constraint:
(7)    (COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(TRUE, x0[1])≥NonInfC∧COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(TRUE, x0[1])≥398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(+(x0[1], -1))∧(U^Increasing(398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(+(x0[1], -1))), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ((U^Increasing(398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ((U^Increasing(398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    ((U^Increasing(398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(x0) → COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(>(x0, 1), x0)
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(>(x0[0], 1), x0[0])), ≥)∧[(-1)Bound*bni_8 + (4)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(TRUE, x0) → 398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(+(x0, -1))
- ((U^Increasing(398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(x₁)) = [2]x₁
POL(COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(x₁, x₂)) = [2]x₂
POL(>(x₁, x₂)) = [-1]
POL(1) = [1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(-1) = [-1]

The following pairs are in P_>:

COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(TRUE, x0[1]) → 398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(+(x0[1], -1))

The following pairs are in P_bound:

398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(x0[0]) → COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(>(x0[0], 1), x0[0])

The following pairs are in P_≥:

398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(x0[0]) → COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(>(x0[0], 1), x0[0])

There are no usable rules.

(16) Complex Obligation (AND)

(17) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

(18) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(19) TRUE

(20) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(TRUE, x0[1]) → 398_0_APPENDNEWLIST_CONSTANTSTACKPUSH(x0[1] + -1)

The set Q is empty.

(21) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPtoQDPProof (SOUND transformation)

(9) Obligation:

(10) QDPSizeChangeProof (EQUIVALENT transformation)

(11) YES

(12) Obligation:

(13) SCCToIDPv1Proof (SOUND transformation)

(14) Obligation:

(15) IDPNonInfProof (SOUND transformation)

(16) Complex Obligation (AND)

(17) Obligation:

(18) IDependencyGraphProof (EQUIVALENT transformation)

(19) TRUE

(20) Obligation:

(21) IDependencyGraphProof (EQUIVALENT transformation)

(22) TRUE